es:ES, Cmd:Type, In:AbsInterface(Cmd), isupdate:(Cmd), Sys, Out:AbsInterface(Top).
(E(In) r E(Sys))
 (E(Out) r E(Sys))
 (e:E(In). (((isupdate(In(e)))))  ((e  Out)))
 (f:sys-antecedent(es;Sys).
 (u:E(Sys). (f(u) = u  E)  ((u  In)))
  fifo-antecedent(es;Sys;f)
  (e:E(In). f(e) = e  E)
  (chain:(E(Sys)(Id List)).
  chain-consistent(f;chain)
   (a1, a2:E(Sys), e1, e2:E(In).
   ((isupdate(In(e1))))
    ((isupdate(In(e2))))
    e1 is f*(a1)
    e2 is f*(a2)
    (a1 <loc a2)
    (e:E(Sys). (e loc e2  & e1 is f*(e) & e is f*(a1)))))) 

latex

Up	abstract chain replication
Definitions	t  T, chain-consistent(f;chain), x:AB(x), E(X), b, y is f*(x), (e <loc e'), Id, type List, f(a), E, s = t, x:A. B(x), fifo-antecedent(es;Sys;f), sys-antecedent(es;Sys), AbsInterface(A), e  X, X(e), A, P  Q, , Top, Type, ES, sys-order(es; Sys; f), EState(T), a:A fp B(a), , strong-subtype(A;B), EqDecider(T), Unit, left + right, IdLnk, x:A  B(x), EOrderAxioms(E; pred?; info), kindcase(k; a.f(a); l,t.g(l;t) ), Knd, loc(e), kind(e), Msg(M), , val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), r  s, e < e', constant_function(f;A;B), SWellFounded(R(x;y)), , pred!(e;e'), x,y. t(x;y), !Void(), x:A.B(x), S  T, suptype(S; T), first(e), <a, b>, pred(e), x.A(x), x. t(x), P & Q, {x:A| B(x)} , let x,y = A in B(x;y), t.1, False, ff, inr x , tt, inl x , True, case b of inl(x) => s(x) | inr(y) => t(y), e c e', if b then t else f fi , P  Q, e loc e' , x:A. B(x), a < b, hd(l), L1  L2, adjacent(T;L;x;y), (x  l), no_repeats(T;l), y=f*(x) via L, (e < e'), loc(e), f**(e), e(e1,e2].P(e), @e(xv), (last change to x before e), A c B, pred(e), P  Q, P  Q, lastchange(x;e), es-init(es;e), {i..j}, x  dom(f), ||as||, #$n, Dec(P), e<e'.P(e), ee'.P(e), e<e'. P(e), ee'.P(e), e[e1,e2).P(e), e[e1,e2).P(e), e[e1,e2].P(e), e[e1,e2].P(e), e(e1,e2].P(e), Atom$n, l_disjoint(T;l1;l2), MaName, x before y  l, x << y, x <<= y, {T}, SQType(T), s ~ t, as @ bs, kind(e), first(e), source(l), destination(l), isrcv(e), es-first-from(es;e;l;tg), isrcv(k), last(L), T, f(x)?z, , b | a, a ~ b, a  b, a <p b, a < b, x f y, xL. P(x), (xL.P(x)), r < s, q-rel(r;x), Outcome, SqStable(P), a =!x:T. Q(x), InvFuns(A;B;f;g), Inj(A;B;f), IsEqFun(T;eq), Refl(T;x,y.E(x;y)), Sym(T;x,y.E(x;y)), Trans(T;x,y.E(x;y)), AntiSym(T;x,y.R(x;y)), Connex(T;x,y.R(x;y)), CoPrime(a,b), Ident(T;op;id), Assoc(T;op), Comm(T;op), Inverse(T;op;id;inv), BiLinear(T;pl;tm), IsBilinear(A;B;C;+a;+b;+c;f), IsAction(A;x;e;S;f), Dist1op2opLR(A;1op;2op), fun_thru_1op(A;B;opa;opb;f), FunThru2op(A;B;opa;opb;f), Cancel(T;S;op), monot(T;x,y.R(x;y);f), IsMonoid(T;op;id), IsGroup(T;op;id;inv), IsMonHom{M1,M2}(f), a  b, IsIntegDom(r), IsPrimeIdeal(R;P), f  g, sender(e)
Lemmas	es-fix-equal-E-interface, es-fix-equal, es-le-causle, decidable es-causle, es-fix-connected, es-causl weakening, es-locl transitivity2, es-le weakening, es-locl irreflexivity, sq stable from decidable, decidable assert, fun-connected-fixedpoint, decidable es-locl, es-le-not-locl, all functionality wrt iff, implies functionality wrt iff, squash wf, chain-consistent-after-input, decidable es-le, es-pred wf, iff wf, rev implies wf, es-isrcv-loc, es-le-loc, guard wf, es-loc-pred, es-locl-iff, chain-path-ordered, chain-consistent-continuity, chain-order-le wf, Id sq, chain-order-total2, decidable equal Id, es-le weakening eq, decidable es-E-equal, es-causle-le, es-le wf, fun-connected weakening eq, es-loc wf, es-causl wf, es-locl wf, fun-path wf, fun-connected wf, chain-consistent wf, fifo-antecedent wf, es-E-interface-subtype rel, es-causle wf, sys-antecedent wf, es-interface-val wf2, true wf, false wf, btrue wf, bfalse wf, es-interface wf, es-E-interface wf, es-is-interface wf, es-E wf, deq wf, EOrderAxioms wf, kind wf, Msg wf, nat wf, val-axiom wf, cless wf, qle wf, bool wf, Knd wf, kindcase wf, IdLnk wf, constant function wf, loc wf, not wf, assert wf, first wf, top wf, unit wf, pred! wf, strongwellfounded wf, member wf, rationals wf, Id wf, EState wf, subtype rel wf, event system wf, chain-consistent-order